Pointer Coercions

In addition to pointer subtyping, Cyclone provides a number of coercions which allow you to convert a pointer value from one type to another. For instance, you can coerce a thin pointer with 42 elements to a fat pointer:

  int arr[42];
  int *@thin @numelts(42) p = arr;
  int *@fat pfat = p;

As another example, you can coerce a thin, zero-terminated pointer to a fat, zero-terminated pointer:

  int strlen(char *@zeroterm s) {
    char *@fat @zeroterm sfat = s;
    return numelts(s);
  }

In both cases, the compiler inserts code to convert from the thin representation to an appropriate fat representation. In the former case, the bounds information can be calculated statically. In the latter case, the bounds information is calculated dynamically (by looking for the zero that terminates the sequence.) In both cases, the coercion is guaranteed to succeed, so the compiler does not emit a warning.

In other cases, a coercion can cause a run-time exception to be thrown. For instance, if you attempt to coerce a @nullable pointer to a @notnull pointer, and the value happens to be NULL, then the exception Null_Exception is thrown. In general, the compiler will warn you when you try to coerce from one pointer representation to another where a run-time check must be inserted, and that check might fail. A dataflow analysis is used to avoid some warnings, but in general, it’s not smart enough to get rid of all of them. In these cases, you can explicitly cast the pointer from one representation to the other, and the compiler will not generate a warning (though it will still insert the run-time check to ensure safety.)

Here is a list of some of the coercions that are possible:

• T can be coerced to S when T is a subtype of S.
• T*@nullable can be coerced to T*@notnull but might throw an exception at run-time.
• T*@thin@numelts(c) can be coerced to T*@fat when c is a constant expression.
• T*@fat can be coerced to T*@thin @numelts(c) when c is a constant expression, but might throw an exception at run-time.
• T*@thin@zeroterm can be coerced to T*@fat@zeroterm and vice versa.
• T*@thin@zeroterm can be coerced to const T*@fat@nozeroterm.
• T*@thin@zeroterm can be coerced to T*@fat@nozeroterm, but access to the trailing zero is lost.